PRISM
=====
Version: 4.5.dev
Date: Fri Feb 26 16:17:06 CET 2021
Hostname: christopher
Memory limits: cudd=4g, java(heap)=11g
Command line: prism -javamaxmem 11g -cuddmaxmem 4g -heuristic speed -e 1e-6 -maxiters 1000000 wlan.6.prism wlan.props --property cost_min -const COL=0
Parsing model file "wlan.6.prism"...
Type: MDP
Modules: medium station1 station2
Variables: col c1 c2 x1 s1 slot1 backoff1 bc1 x2 s2 slot2 backoff2 bc2
Parsing properties file "wlan.props"...
7 properties:
(1) "collisions": Pmax=? [ F col=COL ]
(2) "cost_max": R{"cost"}max=? [ F s1=12&s2=12 ]
(3) "cost_min": R{"cost"}min=? [ F s1=12&s2=12 ]
(4) "num_collisions": R{"collisions"}max=? [ F s1=12&s2=12 ]
(5) "sent": P>=1 [ F s1=12&s2=12 ]
(6) "time_max": R{"time"}max=? [ F s1=12&s2=12 ]
(7) "time_min": R{"time"}min=? [ F s1=12&s2=12 ]
---------------------------------------------------------------------
Model checking: "cost_min": R{"cost"}min=? [ F s1=12&s2=12 ]
Model constants: COL=0
Warning: Switching to sparse engine and (backwards) Gauss Seidel (default for heuristic=speed).
Building model...
Model constants: COL=0
Computing reachable states...
Reachability (BFS): 195 iterations in 0.31 seconds (average 0.001574, setup 0.00)
Time for model construction: 0.423 seconds.
Type: MDP
States: 5007548 (1 initial)
Transitions: 11475748
Choices: 6350470
Transition matrix: 20377 nodes (8 terminal), 11475748 minterms, vars: 47r/47c/7nd
Prob0A: 3101 iterations in 54.92 seconds (average 0.017711, setup 0.00)
Prob1E: 3102 iterations in 65.31 seconds (average 0.021055, setup 0.00)
Warning: PRISM hasn't checked for zero-reward loops.
Your minimum rewards may be too low...
goal = 1, inf = 0, maybe = 5007547
Computing remaining rewards...
Engine: Sparse
Building sparse matrix (transitions)... [n=5007548, nc=6350469, nnz=11475747, k=3] [174.7 MB]
Building sparse matrix (transition rewards)... [n=5007548, nc=6350469, nnz=1226047, k=3] [57.4 MB]
Creating vector for state rewards... [38.2 MB]
Creating vector for inf... [38.2 MB]
Allocating iteration vectors... [2 x 38.2 MB]
TOTAL: [384.8 MB]
Starting iterations...
Iteration 96: max relative diff=0.483333, 5.02 sec so far
Iteration 192: max relative diff=0.315217, 10.05 sec so far
Iteration 288: max relative diff=0.233871, 15.07 sec so far
Iteration 384: max relative diff=0.185897, 20.10 sec so far
Iteration 480: max relative diff=0.154255, 25.13 sec so far
Iteration 576: max relative diff=0.131818, 30.15 sec so far
Iteration 672: max relative diff=0.115079, 35.16 sec so far
Iteration 768: max relative diff=0.102113, 40.17 sec so far
Iteration 864: max relative diff=0.091772, 45.18 sec so far
Iteration 960: max relative diff=0.083333, 50.18 sec so far
Iteration 1056: max relative diff=0.076316, 55.19 sec so far
Iteration 1152: max relative diff=0.070388, 60.24 sec so far
Iteration 1249: max relative diff=0.065169, 65.29 sec so far
Iteration 1346: max relative diff=0.060797, 70.32 sec so far
Iteration 1443: max relative diff=0.056974, 75.35 sec so far
Iteration 1540: max relative diff=0.053506, 80.37 sec so far
Iteration 1637: max relative diff=0.050523, 85.39 sec so far
Iteration 1735: max relative diff=0.047776, 90.44 sec so far
Iteration 1833: max relative diff=0.045383, 95.48 sec so far
Iteration 1931: max relative diff=0.043155, 100.51 sec so far
Iteration 2029: max relative diff=0.041135, 105.53 sec so far
Iteration 2127: max relative diff=0.039349, 110.53 sec so far
Iteration 2226: max relative diff=0.037662, 115.57 sec so far
Iteration 2325: max relative diff=0.036115, 120.60 sec so far
Iteration 2424: max relative diff=0.034689, 125.62 sec so far
Iteration 2523: max relative diff=0.033372, 130.63 sec so far
Iteration 2622: max relative diff=0.032151, 135.65 sec so far
Iteration 2722: max relative diff=0.030983, 140.69 sec so far
Iteration 2822: max relative diff=0.029928, 145.73 sec so far
Iteration 2922: max relative diff=0.028942, 150.77 sec so far
Iteration 3022: max relative diff=0.027992, 155.81 sec so far
Iterative method: 3115 iterations in 164.68 seconds (average 0.051522, setup 4.18)
Value in the initial state: 7625.0
Time for model checking: 284.931 seconds.
Result: 7625.0 (value in the initial state)
Overall running time: 285.632 seconds.
---------------------------------------------------------------------
Note: There were 2 warnings during computation.